\documentclass[10pt,a4paper]{article}

%% For typesetting theorems and some math symbols.
\usepackage{amssymb}
\usepackage{amsthm}

\usepackage{fullpage}

\title{Featherweight Ownership and Immutability Generic Java - Technical Report}

\author{Yoav Zibin \texttt{yoav.zibin@gmail.com}}

\date{}




\input{commands}


\begin{document}


\maketitle


\lstset{language=java,basicstyle=\ttfamily\small}

%\chapter{Featherweight Ownership and Immutability Generic Java}
\section{Introduction}
This technical report contains proofs that were omitted from our paper entitled
    ``Ownership and Immutability in Generic Java''.
Please read the paper first, and only then proceed to reading this technical report,
    because this technical report is not self contained.
We only include a summary of the syntax (\Ref{Figure}{syntax}),
    subtyping rules (\Ref{Figure}{subtyping}),
    expression typing rules (\Ref{Figure}{expressions}),
    and reduction rules (\Ref{Figure}{reduction}).

We begin with some definitions.
A \emph{rule} has the form~$\typerule{A}{B}$, where~$A$ is the \emph{assumption}
    and $B$ is the \emph{conclusion}.
If~$A$ is empty, we also call the rule an \emph{axiom}.
An \emph{instance} of a rule/assumption/conclusion is any substitution of variables in the rule.
A \emph{derivation sequence} is a sequence of elements (each element is an instance of a conclusion),
    where the assumptions needed for each element appear as previous elements in the sequence.

An expression/type is called \emph{closed} if it does not contain
    any free variables (such as wildcards, \this, \hI, \hO, or \This).

The length of a sequence~$\ol{\hx}$ is written~$\#(\ol{\hx})$,

To define \code{\ftype{}(e,f,T)} and \code{\mtype{}(e,f,T)}, we use the auxiliary function~\substitute:
\[
    \substitute(\he,\code{C<MO,IP>},\hT) =
        \begin{cases}
        \code{error} & \Ofn{\hT}=\This \text{~and~} \code{z}=\code{error} \\
        [\code{z}/\This,\code{MO}/\hO,\code{IP}/\hI]\hT & \text{otherwise} \\
        \end{cases}
    \gap
    \code{z}=
        \begin{cases}
        \hl & \he=\hl \\
        \This & \he=\this \\
        \code{error} & \text{otherwise} \\
        \end{cases}
\]
Formally, $\code{\ftype{}(e,f,C<MO,IP>)}=\substitute(\he,\code{C<MO,IP>},\ftype{}(\hf,\hC))$,
    and similarly for~\mtype.

Given an expression~\he, we define~$K(\he)$ to be the set
    of all ongoing constructors in~\he, i.e., all locations in subexpressions~\code{e;return l}.
Formally,
\[
K(\he) =
\begin{cases}
    K(\code{e'}) \cup \{ l \} & \text{if~}\he=(\code{e';return l}) \\
    K(\code{e'}) & \text{if~}\he=(\code{e'.f}) \\
    K(\code{e'}) \cup K(\code{e"}) & \text{if~}\he=(\code{e'.f=e"}) \\
    \cup K(\ol{\he'}) & \text{if~}\he=(\code{new N}\hparen{\ol{\he'}}) \\
    K(\code{e"}) \cup K(\ol{\he'}) & \text{if~}\he=(\code{e".m}\hparen{\ol{\he'}}) \\
    \end{cases}
\]

A heap~$H$ is \emph{well-typed for~$K$} if it satisfies two conditions:
(i)~Each field location is a subtype (using~$K,\Gamma_H$) of the declared field type,
    i.e., for every location~\hl, where $H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}$ and~$\fields{}(\hC)=\ol{\hf}$,
        and
        for every field~$\hf_i$, we have that either $\hv_i=\code{null}$ or
        $K,\Gamma_H \vdash \Gamma_H(\hv_i) \st \ftype{}(\hl,\hf_i,\code{C<NO,NI>})$.
(ii)~There is a linear order~$\Tprec$ over~$\dom{}(H)$ such that for every location~\hl,
        $\OwnerH{\hl}=\World$ or $\OwnerH{\hl} \TprecNotEqual \hl$, and $\IfnH{\hl}=\Mutable$ or $\CookerH{\hl} \Tprec \hl$.

\begin{smaller}
\input{formal-syntax}
\input{formal-subtyping}
\input{formal-typing}
\input{formal-reduction}
\end{smaller}


\section{Subtyping}

First we prove some lemmas regarding subtyping.
%Owners are preserved by subtyping (i.e., ownership is invariant).

\begin{Lemma}[Owners-Invariant]
If $K,\Gamma \vdash \code{C<MO,IP>}\st\code{C'<MO',IP'>}$, then\\
    (i)~$\code{MO'}\neq\code{?} \Rightarrow \code{MO}=\code{MO'}$,\\
    (ii)~$(\code{IP'}\neq\Immut_\hl \text{~or~} (\code{IP'}=\Immut_\hl \text{~and~} (\hl \not\OprecNotEqual \code{MO'} \text{~or~} \hl \not\in K)) \Rightarrow K,\Gamma \vdash \code{IP} \st \code{IP'}$, \\
    (iii)~\code{C} is a subclass of~\code{C'},\\
    (iv)~$K,\Gamma \vdash \code{D<MO,IP>}\st\code{D<MO',IP'>}$ for any class~\code{D},\\
    (v)~$K,\Gamma \vdash \code{D<l,IP>}\st\code{D<l,IP'>}$ for any class~\code{D} and~$\code{MO'} \Oprec \hl$.
\end{Lemma}
\begin{proof}
In this proof we omit~$K,\Gamma \vdash$ because the context~$K,\Gamma$ is clear.
First note that due to \RULE{S13}, it is not the case that $\code{IP} \st \code{IP'}$.
Therefore, we need parts (ii) and (iv)--(v), which connects \code{IP} and \code{IP'} in other ways.

(i)~All subtyping rules maintain the same owner parameter, except
    \RULE{S9},
        thus if~$\code{MO'}\neq\code{?}$, then the owner must be preserved.

(ii)~All subtyping rules maintain that~$\code{IP} \st \code{IP'}$ except \RULE{S13}.
If~$\hl \not\OprecNotEqual \code{MO'}$ then we cannot use \RULE{S13}.
If~$\hl \not\in K$ then (from \RULE{S12})~$\Immut \st \code{IP'}$,
    and if the proof used \RULE{S13} then~$\code{C<MO,IP>}\st\code{C<MO,Immut>}$, thus~$\code{IP}\st\Immut\st\code{IP'}$.

(iii)~All rules maintain the same class, and \RULE{S4} permits subclassing.

(iv)~We create a new derivation sequence where instances of rule~\RULE{S4} are deleted,
    and all occurrences of~\hC are replaced with \code{D}.

(v)~Similarly to part (iv), we delete~\RULE{S4} and~\RULE{S9}, replace~\hC with \code{D},
        and replace \code{MO} and \code{MO'} with \hl.
    The only rule where the owner matters is~\RULE{S13}:\[
    \typerule{
\hl' \OprecNotEqual \code{MO'}
}{
  K,\Gamma \vdash \hC\hgn{\code{MO'},\Immut} \st \hC\hgn{\code{MO'},\Immut_{\hl'}}
}
\]and we have that~$\code{MO'} \Oprec \hl$, therefore~$\hl' \OprecNotEqual \hl$.
\end{proof}

\begin{Lemma}[subtyping2]
If $K,\Gamma \vdash \code{C<MO,IP>}\st\code{C'<MO,IP'>}$, then
    for any class~\code{D} and any owner parameter~$\code{W}$ such that~$\code{W} = \hO ~|~ \World$,
    we have that
    \[
    K,\Gamma \vdash \code{D<}[\code{MO}/\hO]\code{W},[\code{IP}/\hI]\code{Z>}\st\code{D<}[\code{MO}/\hO]\code{W},[\code{IP'}/\hI]\code{Z>}.
    \]
\end{Lemma}
\begin{proof}
If~$\code{Z}\neq\hI$ then obviously~$\code{D<}[\code{MO}/\hO]\code{W},\code{Z>}=\code{D<}[\code{MO}/\hO]\code{W},\code{Z>}$.
If~$\code{Z}=\hI$ then we need to prove that
    $K,\Gamma \vdash \code{D<}[\code{MO}/\hO]\code{W},\code{IP>}\st\code{D<}[\code{MO}/\hO]\code{W},\code{IP'>}$.
Because~$\code{MO} \Oprec \World$ and~$\code{W} = \hO ~|~ \World$, then
    $\code{MO} \Oprec [\code{MO}/\hO]\code{W}$.
Therefore, we can apply \Ref{Lemma}{Owners-Invariant} part (v).
\end{proof}


\begin{Lemma}[isTransitive]
If $K,\Gamma \vdash \code{C<MO,IP>}\st\code{C'<MO,IP'>}$, both types are closed,
   $\isTransitive(\bot,\Gamma,\code{C'<MO,IP'>})$ and~$\code{IP'} \st \Raw$,
   then~$\code{IP}=\code{IP'}$.
\end{Lemma}
\begin{proof}
If $\code{IP'} = \Mutable$ then obviously~$\code{IP} = \Mutable$.
Otherwise $\code{IP'}=\Immut_\hl$ and~$\hl \in K$ (because~$\code{IP'} \st \Raw$).
From definition of $\isTransitive(\bot,\Gamma,\code{C'<MO,IP'>})$,
    $\hl \not \OprecNotEqual \code{MO}$,
    thus \RULE{S13} cannot be applied, and that is the only applicable rule where~$\Immut_\hl$
    appears as a supertype (because \RULE{S12} cannot be applied since~$\hl \in K$),
    thus~$\code{IP}=\code{IP'}$.
\end{proof}

The next lemma shows that if~$\he'$ was reduced to~$\he$ (therefore the type of \he is a subtype of~$\he'$),
    then~$\he$ can call any method that~$\he'$ could.
Phrased differently, if~$\he'$ satisfies a method's guard then~$\he$ would as well.
\begin{Lemma}[Guard]
If $K,\Gamma \vdash \code{C<MO,IP>}\st\code{C'<MO,IP'>}$, and both types are closed, then\\
    (i)~$K,\Gamma \vdash \code{IP'} \st \Mutable \Rightarrow K,\Gamma \vdash \code{IP} \st \Mutable$,\\
    (ii)~$K,\Gamma \vdash \code{IP'} \st \Immut \Rightarrow K,\Gamma \vdash \code{IP} \st \Immut$,\\
    (iii)~$\isTransitive(\bot,\Gamma,\code{C'<MO,IP'>}) \text{~and~} K,\Gamma \vdash \code{IP'} \st \Raw \Rightarrow K,\Gamma \vdash \code{IP} \st \Raw$,\\
    (iv)~if~$\code{IG}=\Raw \Rightarrow \isTransitive(\bot,\Gamma,\code{C'<MO,IP'>})$,
        where~$\code{IG}=\ReadOnly ~|~ \Immut ~|~ \Mutable ~|~ \Raw$,
        then
        $K,\Gamma \vdash \code{IP'} \st \code{IG} \Rightarrow K,\Gamma \vdash \code{IP} \st \code{IG}$.
\end{Lemma}
\begin{proof}
(i)~Trivial because we must have that $\code{IP'} = \code{IP} = \Mutable$ or ($\code{IP'} = \code{IP} = \hI$ and $\hI:\Mutable \in \Gamma$).

(ii)~If $\code{IP'}\neq\Immut_\hl$ then from \Ref{Lemma}{Owners-Invariant} part (ii), we have~$K,\Gamma \vdash \code{IP} \st \code{IP'}$,
    and from transitivity~$\code{IP} \st \code{IP'} \st \Immut \Rightarrow \code{IP} \st \Immut$.
Otherwise, $\code{IP'}=\Immut_\hl$, and because~$\code{IP'} \st \Immut$, from \RULE{S11} we must have that~$\hl \not \in K$,
    and from \Ref{Lemma}{Owners-Invariant} part (ii), we proved~$K,\Gamma \vdash \code{IP} \st \code{IP'}$,

(iii)~From \Ref{Lemma}{isTransitive} we know that~$\code{IP}=\code{IP'}$ thus~$\code{IP} \st \Raw$.

(iv) Stems from parts (vi)--(viii) and the fact that for any~$\code{IP} \st \ReadOnly$.
\end{proof}



If the cooker is not inside the owner, then subtypes are not over-approximation
        (i.e., they preserve the same cooker).
% We did not use this lemma in the proofs, but "over-approximation" is mentioned in the paper, so I wanted to prove it.
\begin{Lemma}[Exact-Cooker]
If $K,\Gamma \vdash \code{C<MO,IP>} \st \code{C'<NO,Immut}_{\hl}\code{>}$,
    $\hl \not\OprecNotEqual \code{NO}$, and $\hl \in K$,
    then~$\code{IP}=\code{Immut}_{\hl}$.
\end{Lemma}

\begin{proof}
The only subtyping rule where the supertype has a cooker~$\code{Immut}_{\hl}$
    are rules \RULE{S12} and~\RULE{S13}, and
    they can't be applied because we assumed that~$\hl \not\OprecNotEqual \code{NO}$ and~$\hl \not\in K$.
    Thus only the reflexivity rule can be applied.
Note that rule~$K,\Gamma \vdash \hI \st \Gamma(\hI)$ cannot be applied because we assume that~$\Gamma(\hI)$ is a method guard~$\code{IG}$,
    and $\code{IG} \neq \code{Immut}_{\hl}$ because according to our syntax~\[
        \code{IG}=\ReadOnly ~|~ \Immut ~|~ \Mutable ~|~ \Raw.
        \]
\end{proof}




Next we prove a substitution lemma:
    substituting~\hI,~\hO, or~\This, does not change the subtype relation.
\begin{Lemma}[subtyping-substitute]
If~$K,\Gamma \vdash \hT \st \hT'$ then for every~$\code{IP},\code{MO},\code{MO'}$
    such that~$\code{IP} \st \Gamma(\hI)$,
        we have that \[
        K,\Gamma \vdash [\code{IP}/\hI,\code{MO}/\hO,\code{MO'}/\This](\hT \st \hT').
        \]
\end{Lemma}
\begin{proof}
Let~$S$ denote the derivation sequence for~$K,\Gamma \vdash \hT \st \hT'$,
    and~$S_I$ for~$\code{IP} \st \Gamma(\hI)$.
Let~$S'$ be a new sequence in which we do the substitution~$[\code{IP}/\hI,\code{MO}/\hO,\code{MO'}/\This]$
    on every element in~$S$,
    and let~$S"$ be the sequence starting with~$S_I$ followed by~$S'$.
The last element in~$S$ is~$K,\Gamma \vdash \hT \st \hT'$, therefore the last element in~$S'$ and~$S"$ is
    what we need to prove:~$K,\Gamma \vdash [\code{IP}/\hI,\code{MO}/\hO,\code{MO'}/\This](\hT \st \hT')$.
Next we show that~$S"$ is a legal derivation sequence by showing that each element is a legal consequence of previous elements
    (by induction on the size of~$S"$).
Elements from~$S_I$ are of course legal.
By induction we proved the first~$n-1$ elements are legal,
    and we now prove that element~$n$ is legal (i.e., a legal consequence of previous elements).
Let the corresponding element in~$S$ be~$\hU \st \hU'$,
    and element~$n$ is~$[\code{IP}/\hI,\code{MO}/\hO,\code{MO'}/\This](\hU \st \hU')$.
(i)~If the element is an instance of rules~\RULE{S5}--\RULE{S7} or~\RULE{S10}--\RULE{S12},
    then substitution did not change the element.
(ii)~If the element is an instance of rule~\RULE{S1} then we replaced it
    with~$[\code{IP}/\hI](\hI \st \Gamma(\hI)) = \code{IP} \st \Gamma(\hI)$,
        which is the last element of~$S_I$.
(iii)~If the element is an instance of any other rule,
    then a simple application of the induction hypothesis proves the element is legal.
\end{proof}



We now prove that substitution preserves subtyping.
\begin{Lemma}[subtyping-substitute2]
If~$K,\Gamma \vdash \hT \st \hT'$, \hT and $\hT'$ are closed,
    then for~($\he=\bot$ and $\Ofn{\code{\hT"}}\neq\This$) or~$\he=\hl$,~$\Ofn{\hT} \Oprec \hl$, we have that:\\
    (i)~$K,\Gamma \vdash \substitute(\he,\hT,\hT") \st \substitute(\he,\hT',\hT")$,\\
    (ii)~$K,\Gamma \vdash \ftype{}(\he,\hf,\hT) \st \ftype{}(\he,\hf,\hT')$,\\
    (iii)~let~$\mtype{}(\he,\hf,\hT)=\ol{\code{T}}\rightarrow\code{T}_0$ and~$\ftype{}(\he,\hf,\hT')=\ol{\code{T}'}\rightarrow\code{T}'_0$,
        then~$K,\Gamma \vdash \hT_i \st \hT'_i$ for~$i=0,\ldots,\#(\ol{\code{T}})$.
\end{Lemma}
\begin{proof}
From \Ref{Lemma}{Owners-Invariant} part (i) and the fact that \hT and $\hT'$ are closed (no wildcards),
    then~$\Ofn{\hT}=\Ofn{\hT'}$.
Let~$\hT = \code{C<MO,IP>}$ and~$\hT' = \code{C'<MO,IP'>}$.

Recall that~$\code{\ftype{}(e,f,C<MO,IP>)}=\substitute(\he,\code{C<MO,IP>},\ftype{}(\hf,\hC))$,
    and similarly for~\mtype.
Therefore, parts (ii) and (iii) follow from part (i),
    and the fact that~$\ftype{}(\hf,\hC) = \ftype{}(\hf,\hC')$
    and~$\mtype{}(\hm,\hC) = \mtype{}(\hm,\hC')$ (i.e., subclassing cannot change method signature or field type).

We now prove part (i).
From the definition of $\substitute$, and because~($\he=\bot$ and $\Ofn{\code{\hT"}}\neq\This$) or~$\he=\hl$,
    we have that~$\substitute{}(\he,\hT,\hT") = [\code{e}/\This,\code{MO}/\hO,\code{IP}/\hI]\hT"$.

Let~$\hT" = \code{D<MO",IP">}$.
Because~$K,\Gamma \vdash \hT \st \hT'$, from \Ref{Lemma}{Owners-Invariant} part (v),
    \beq{subtyping1}
    K,\Gamma \vdash \code{D<\hl',IP>} \st \code{D<\hl',IP'>} \text{~if~}\code{MO} \Oprec \hl'
    \eeq
    (note that~$\hl'$ can be \code{MO} or \code{World}).
We need to prove that~$K,\Gamma \vdash \substitute{}(\he,\hT,\hT") \st \substitute{}(\he,\hT',\hT")$,
    i.e.,~$K,\Gamma \vdash [\code{e}/\This,\code{MO}/\hO,\code{IP}/\hI]\hT" \st [\code{e}/\This,\code{MO}/\hO,\code{IP'}/\hI]\hT"$.


If~$\code{IP"} \neq \hI$ then from reflexivity
    $K,\Gamma \vdash [\code{e}/\This,\code{MO}/\hO]\hT" \st [\code{e}/\This,\code{MO}/\hO]\hT"$.

Consider now the case that~$\code{IP"} = \hI$.
We need to show that
    \beq{subtyping2}
    K,\Gamma \vdash \code{D<}[\code{e}/\This,\code{MO}/\hO]\code{MO",IP>} \st \code{D<}[\code{e}/\This,\code{MO}/\hO]\code{MO",IP'>}
    \eeq
Because~$\code{MO"}=\hO~|~\World~|~\This$ and
    $\he=\bot$ or~$\he=\hl$, we have that
    \beq{subtyping3}
    \code{MO} \Oprec [\code{e}/\This,\code{MO}/\hO]\code{MO"}
    \eeq
From \eq{subtyping1} and \eq{subtyping3}, we proved \eq{subtyping2}.

\end{proof}


\begin{Lemma}[invokeSubtype]
If $K,\Gamma \vdash \code{C<MO,IP>}\st\code{C'<MO,IP'>}$, and both types are closed,
    and
    \beqst
    &\mtype{}(\bot,\hm,\code{C'<MO,IP'>})=\ol{\code{T'}}\rightarrow\code{U}\\
    &\mtype{}(\bot,\hm,\code{C<MO,IP>})=\ol{\code{T}}\rightarrow\code{U}\\
    &\mguard{}(\hm,\code{C'})=\code{IG}\\
    &K,\Gamma \vdash \code{IP'} \st \code{IG}\\
    &\code{IG}=\Raw \Rightarrow \isTransitive(\bot,\Gamma,\code{C'<MO,IP'>})\\
    \eeq
    then
    (i)~$K,\Gamma \vdash {\code{T}_i} \st {\code{T'}_i}$ and~$K,\Gamma \vdash {\code{T'}_i} \st {\code{T}_i}$, and
    (ii)~for any type~\code{T"}, if~$K,\Gamma \vdash {\code{T"}} \st {\code{T'}_i}$ then~$K,\Gamma \vdash {\code{T"}} \st {\code{T}_i}$.
\end{Lemma}
\begin{proof}
Part (i) implies that~$\code{T'}_i$ and~$\code{T}_i$ are equivalent.
Part (ii) follows directly from part (i) using transitivity rule~\RULE{S3}.

Let~$\mtype{}(\hm,C) = \mtype{}(\hm,C') = \ol{\code{FT}}\rightarrow\code{V}$,
    $\code{FT}_i = \code{D<FO,IP">}$.
Note that~$\code{T'}_i = [\code{MO}/\hO,\code{IP'}/\hI]\code{FT}_i$
    and~$\code{T}_i = [\code{MO}/\hO,\code{IP}/\hI]\code{FT}_i$.
Therefore, if~$\code{IP"}\neq\hI$ then~$\code{T'}_i=\code{T}_i$, qed.

Thus,~$\code{IP"}=\hI$,~$\code{T'}_i = \code{D<MO",IP'>}$,~$\code{T}_i = \code{D<MO",IP>}$,
    where~$\code{MO} \Oprec \code{MO"}$ (because~$\code{FO}$ is either \hO or \World, but it cannot be \This).
From \Ref{Lemma}{subtyping-substitute2} part (iii),~$\code{T}_i \st \code{T'}_i$.

If~$\code{IG}=\ReadOnly$, then FOIGJ ensures that~\hI does not appear in method parameters,
    i.e., we must have that~$\code{IP"}\neq\hI$.
If~$\code{IG}=\Mutable$, then~$\code{IP'}=\code{IP}=\Mutable$ (because~$\code{IP'} \st \code{IG}$),
    thus~$\code{T'}_i=\code{T}_i$,.
If~$\code{IG}=\Immut$, then~$\code{IP'} \st \Immut$ (because~$\code{IP'} \st \code{IG}$),
    thus from \Ref{Lemma}{Guard} part (ii),~$\code{IP} \st \Immut$,
    i.e.,~$\code{IP} \st \code{IP'} \st\code{IP}$.
If~$\code{IG}=\Raw$, then~$\isTransitive(\bot,\Gamma,\code{C'<MO,IP'>})$, and~$\code{IP'} \st \Raw$,
    thus from \Ref{Lemma}{isTransitive} we have that~$\code{IP'}=\code{IP}$.
\end{proof}


\section{Typing}


We next prove that a closed expression has a closed type.
\begin{Lemma}[closed]
If~$K,\Gamma \vdash \he" : \hT"$ and $\he"$ is closed and $\he"\neq\code{null}$, then $\hT"$ is closed.
\end{Lemma}
\begin{proof}
Note that \code{null} can have any type $\hT"$ (even an open type) according to rule \RULE{T-null},
    therefore we require that~$\he"\neq\code{null}$.

We prove by induction on the structure of~$\he"$.
\begin{description}
  \item[Value~$\he"=\hv$] Because~$\he"\neq\code{null}$, then~$\hv=\hl$,
    and the type of a location is always closed~$\hC\code{<NO,NI>}$.
  \item[Value~$\he"=\code{e;return l}$] Similarly, the type of a location is always closed.
  \item[Method parameter~$\he"=\hx$] We assumed $\he"$ is closed, thus it does not contain parameters.
  \item[Object creation~$\he"= \code{new C<FO,VI>(}\ol{\he}\code{)}$]
    From \RULE{T-New},~$\hT" =\hC\hgn{\code{FO},\code{VI}}$, and because~$\he"$ is closed then~$\hT"$ must be closed.
  \item[Field access~$\he"=\he.\hf$]
    Because~$K,\Gamma \vdash \he" : \hT"$, from \RULE{T-Field-Access} we have that~$\hT" = \hT$ and
    \[
    K,\Gamma \vdash \he:\code{C<MO,IP>}
        \gap
    \ftype{}(\he,\hf,\code{C<MO,IP>})=\code{T}
    \]
    By induction,~$\code{C<MO,IP>}$ is closed.
    Therefore~$\hT$ does not contains~\hO nor~\hI.
    Next we show it does not contain \This.
    Because $\ftype$ did not return \code{error},
        then either the field did not contain \This, or it was substituted.
    Because $\he\neq\this$ then~$\he=\hl$, and \This was substituted with \hl.

  \item[Field assignment~$\he"=\he.\hf = \code{e'}$]
    Because~$K,\Gamma \vdash \he" : \hT"$, from \RULE{T-Field-Assignment} we have that~$\hT" = \hT'$ and
        $
        K,\Gamma \vdash \code{e'}:\code{T'}
        $
    By induction, \code{T'} is closed.

  \item[Method invocation~$\he"=\he_0\code{.m(}\ol{\he}\code{)}$]
    Because~$K,\Gamma \vdash \he" : \hT"$, from \RULE{T-Invoke} we have that
    \[
    K,\Gamma \vdash \he_0:\code{C<MO,IP>}
        \gap
    \mtype{}(\he_0,\hm,\code{C<MO,IP>})=\ol{\code{T}}\rightarrow\code{T"}
    \]
    By induction~$\code{C<MO,IP>}$ is closed, and similar reasoning to field access
        concludes that \code{T"} is closed.
\end{description}
\end{proof}


\section{Heap}

We now prove that if the heap is well-typed for $K$, then it is well-typed for any subset of $K$.

\begin{Lemma}[well-typed]
Given a heap~$H$ that is well-typed for~$K$,
    then for any~$S \subseteq K$,
    the heap~$H$ is well-typed for~$S$.
\end{Lemma}
\begin{proof}
This is not trivial, because decreasing~$K$ changes the subtyping relation by turning raw objects into immutable.
Recall that a {well-typed} heap~$H$ satisfies:
    (i)~there is a linear order~$\Tprec$ over~$\dom{}(H)$ such that for every location~\hl,
        $\Owner{\hl}=\World$ or $\Owner{\hl} \TprecNotEqual \hl$, and $\Ifn{\hl}=\Mutable$ or $\Cooker{\hl} \Tprec \hl$,
        and
    (ii)~each non-null field location is a subtype of the declared field type.

First, note that the same linear order~$\Tprec$ satisfies (i) for~$H$ is well-typed for~$S$.
Suppose to the contrary that $H$ is not well-typed for $S$, i.e.,
    there is some field location~$\code{l.f}$ of type~\hT that points to an object~\ho of type~\code{T"},
    and~$S,\Gamma_{H} \not \vdash \code{T"} \st \hT$.
Because~$H$ is well-typed for $K$, we have that~$K,\Gamma_{H} \vdash \code{T"} \st \hT$.
Consider the derivation sequence for~$K,\Gamma_{H} \vdash \code{T"} \st \hT$.
We will take this sequence and transform it into a proof that~$S,\Gamma_{H} \vdash \code{T"} \st \hT$,
    which will lead to contradiction.
Specifically, we replace every usage of rule \RULE{S10} ($K,\Gamma_H \vdash \Immut_\hl \st \Raw$)
    with a proof that~$K,\Gamma_H \vdash \Immut_\hl \st \ReadOnly$ (using either \RULE{S10} or \RULE{S11}).
We first claim that this is a valid sequence in~$S,\Gamma_{H}$:
    rules~\RULE{S1}--\RULE{S9} and~\RULE{S13} do not use~$K$ and therefore are identical,
    rule~\RULE{S10} was removed,
    and rules~\RULE{S11}--\RULE{S12} is valid because~$S \subset K$.
We now claim that these sequence proves that~$S,\Gamma_{H} \vdash \code{T"} \st \hT$,
    i.e., that each element in the sequence has previous elements that fulfill the assumptions of the rule.
Consider an element we removed~$\Immut_\hl \st \Raw$.
Note that~\Raw does not appear in~$\hT=\code{C<MO,IP>}$ because it can only appear in a method guard.
The only rule where \Raw appears as a subtype is \RULE{S6},
    and by using transitivity (\RULE{S3}), we have that the only conclusion is that~$\Immut_\hl \st \ReadOnly$,
        and we added that conclusion.
\end{proof}

Next we prove that owner-as-dominator holds in any well-typed heap.
\begin{Lemma}[owner-as-dominator]
If heap~$H$ is well-typed for $K$, then for every location~$\hl \in \dom{}(H)$,
    $
    \hl \mapsto \hC\code{<NO,NI>}\hparen{\ol{\hv}}
    $,
    then either~$\hv_i=\code{null}$ or~$\hl \Oprec \Owner{\hv_i}$.
\end{Lemma}
\begin{proof}
Recall that heap~$H$ is \emph{well-typed for~$K$} if it satisfies two conditions:
(i)~Each field location is a subtype (using~$K,\Gamma_H$) of the declared field type,
    i.e., for every location~\hl, where $H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}$ and~$\fields{}(\hC)=\ol{\hf}$,
        and
        for every field~$\hf_i$, we have that either $\hv_i=\code{null}$ or
        $K,\Gamma_H \vdash \Gamma_H(\hv_i) \st \ftype{}(\hl,\hf_i,\code{C<NO,NI>})$.
(ii)~There is a linear order~$\Tprec$ over~$\dom{}(H)$ such that for every location~\hl,
        $\OwnerH{\hl}=\World$ or $\OwnerH{\hl} \TprecNotEqual \hl$, and $\IfnH{\hl}=\Mutable$ or $\CookerH{\hl} \Tprec \hl$.
From part (ii), we have that the relation~$\Oprec$ is a tree order.

Consider some~$\hv_i \neq \code{null}$, and we will prove that~$\hl \Oprec \Owner{\hv_i}$.
Let
\beqst
    H[\hv_i] &= \code{C'<NO',NI'>}\hparen{\ldots}\\
    \fields{}(\hC) &= \ol{\hf}\\
    \ftype{}(\hf_i,\hC) &= \code{C"<FO,IP>}\\
    \ftype{}(\hl,\hf_i,\hC\code{<NO,NI>}) &= \code{C"<NO",NI">}\\
\eeq
We need to prove that~$\hl \Oprec \code{NO'}$.
Because the heap is well-typed for $K$, then~$K,\Gamma_H \vdash \code{C'<NO',NI'>} \st \code{C"<NO",NI">}$.
From \Ref{Lemma}{Owners-Invariant} part (i), we have that~$\code{NO'} = \code{NO"}$.
According to the syntax,~$\code{FO} = \World ~|~ \This ~|~ \hO$ (the owner of a field cannot be~\hl of course because the class declarations cannot use locations).
By definition of~$\ftype{}(\hl,\hf_i,\hC\code{<NO,NI>})$,
    then~$\code{NO"} = \World ~|~ \hl ~|~ \Owner{\hl}$, respectively.
Thus we proved that \[
    \code{NO'} = \code{NO"} = \World ~|~ \hl ~|~ \Owner{\hl}
    \]
Therefore, because $\hl \Oprec \World$ and $\hl \Oprec \hl$ and $\hl \Oprec \Owner{\hl}$, we proved that $\hl \Oprec \code{NO'}$.
\end{proof}

\section{Reduction}
We consider only expressions that when reduced using the erased operational semantics,
    do not result in \emph{null-pointer exceptions}.
Null-pointer exceptions can be handled by adding special reduction rules that return \code{error},
    but we prefer to leave the reduction process ``stuck".

First we prove that a closed expression reduces in one step to another closed expression.
\begin{Lemma}[reduction-closed]
If~\he is closed and~$K \vdash H,\he \reducesto H',\he'$, then~$\he'$ is closed.
\end{Lemma}
\begin{proof}
Rules~\RULE{R-New}, \RULE{R-Field-Access}, and \RULE{R-Field-assignment} result in a value, which is closed.
Rule~\RULE{R-Invoke} results in an expression, but all free variables~$\ol{\hx}, \this, \This, \hO, \hI$ are substituted
    with locations, \Immut, $\Immut_\hl$, or \Mutable.
The proof of the congruence rules uses the induction hypothesis.
\end{proof}

\begin{Lemma}[constructors]
If~$K \vdash H,\he \reducesto H",\he"$ then
    (i)~$\Gamma_H \subseteq \Gamma_{H"}$,
    (ii)~$K,\Gamma_H \vdash \he' : \hT' \Rightarrow K,\Gamma_{H'} \vdash \he' : \hT'$, and
    (iii)~$K,\Gamma_H \vdash \hT \st \hT' \Rightarrow K,\Gamma_{H'} \vdash \hT \st \hT'$.
\end{Lemma}
\begin{proof}
Trivial.
(i)~None of the reduction rules removes locations or changes the type of a location,
    therefore~$H"$ only includes additional locations.
Parts (ii) and (iii) are trivial from (i).
\end{proof}


\begin{Theorem}[preservation]
  \textbf{(Progress and Preservation)}
    For every closed expression~$\he \neq \hv$, $K$, and $H$,
        if $K,\Gamma_{H} \vdash \he : \hT$ and $H$ is well-typed for~$K \cup K(\he)$,
        then there exists~$H',\he',\hT'$ such that
        (i)~$K \vdash H,\he \reducesto H',\he'$,
        (ii)~$K,\Gamma_{H'} \vdash \he':\hT'$,
        and~$K,\Gamma_{H'} \vdash \hT' \st \hT$,
        (iii)~$H'$ is well-typed for~$K \cup K(\he')$,
        (iv)~\hT, \hT', and $\he'$ are closed.
\end{Theorem}
\begin{proof}
Part (iv) is proved from \Ref{Lemma}{reduction-closed} (we know that~$\grave{\he}$ is closed)
    and from \Ref{Lemma}{closed} (we know that $\hT"$ and $\grave{\hT}$ are closed).

We assume that there are no null-pointer exceptions,
    i.e., that for field access, assignment and method invocation, the receiver is never \code{null}.

It is easy to examine the reduction rules
    and verify there is always at most one applicable reduction rule.
We will split the proof into three stages:
    (i)~\textbf{progress:} there is exactly one applicable reduction rule
        (\Ref{Lemma}{part-progress}),
    (ii)~\textbf{preservation:}~$K,\Gamma_{H'} \vdash \grave{\he}:\grave{\hT}$ and~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$
        (\Ref{Lemma}{part-subtype}), and
    (iii)~$H'$ is well-typed for~$K \cup K(\he')$ (\Ref{Lemma}{part-well-typed}).
\end{proof}


\begin{Lemma}[part-progress]
  \textbf{(Progress)}
    For every closed expression~$\he" \neq \hv$, $H$, and $K$,
        if $K,\Gamma_{H} \vdash \he" : \hT"$ and
        and~$H$ is well-typed for~$K \cup K(\he")$,
        then there exists~$H',\grave{\he}$ such that~$K \vdash H,\he" \reducesto H',\grave{\he}$.
\end{Lemma}
\begin{proof}
We prove by examining the structure of~$\he"$.
Because it is closed and not a value, then according to our syntax, it must have one of the following forms:
\[
    \he.\hf ~|~ \he.\hf = \he ~|~ \he.\hm\hparen{\ol{\he}} ~|~ \hnew ~ \hC\hgn{\code{FO},\code{VI}}\hparen{\ol{\he}}  ~|~ \he\code{;return l}
\]
If the subexpressions are not all values, then
    we can always apply (exactly) one of the congruence rules.
For example, if~$\he" = (\he\code{;return l})$ and~$\he$ is not a value,
    then by induction we can apply \RULE{R-c1}.

Therefore,~$\he"$ has one of the following forms:
\[
    \hv.\hf ~|~ \hv.\hf = \hv ~|~ \hv.\hm\hparen{\ol{\hv}} ~|~ \hnew ~ \hC\hgn{\code{FO},\code{VI}}\hparen{\ol{\hv}}  ~|~ \hv\code{;return l}
\]
Because we assumed we do not have \emph{null pointer exceptions} (in field access, assignment or method invocation), then
    $\he"$ has one of the following forms:
\[
    \hl.\hf ~|~ \hl.\hf = \hv ~|~ \hl.\hm\hparen{\ol{\hv}} ~|~ \hnew ~ \hC\hgn{\code{FO},\code{VI}}\hparen{\ol{\hv}}  ~|~ \hv\code{;return l}
\]
We will next examine the matching five reduction rules
    (\RULE{R-Field-Access},
    \RULE{R-Field-Assignment},
    \RULE{R-Invoke},
    \RULE{R-New},
    \RULE{R-return})
    and show that their assumptions hold.

\begin{description}
  \item[Rule~\RULE{R-Field-Access}]
  \[
  \typerule{
    H[\hl] = \code{C<NO,NI>}\hparen{\ol{\hv}}
        \gap
    \fields{}(\hC)=\ol{\hf}
    }{
    K \vdash H,\hl.\hf_i \reducesto H,\hv_i
    }
    \]
  We assumed that~$K,\Gamma_{H} \vdash \hl.\hf_i : \hT"$,
    therefore from \RULE{T-Field-Access}:
    \[
  K,\Gamma_{H} \vdash \hl:\code{C<MO,IP>}
    \gap
  \ftype{}(\hl,\hf_i,\code{C<MO,IP>})=\hT"
    \]
  From the definitions of~\ftype and~\fields, we know that~$\hf_i \in \fields{}(\hC)$.

  \item[Rule~\RULE{R-Field-Assignment}]
  \[
  \typerule{
  H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}
    \gap
  \fields{}(\hC)=\ol{\hf}
    \gap
  \code{NI}=\Mutable \text{~or~} \Cooker{\hl} \in K
    \gap
  \hv'=\code{null} \text{~or~} \hl \Oprec \Owner{\hv'}
}{
  K \vdash H,\hl.\hf_i = \hv' \reducesto H[\hl \mapsto \code{C<NO,NI>(}[\hv'/\hv_i]\ol{\hv}\code{)}],\hv'
}
    \]
Because~$H$ is well-typed for $K$, then from \Ref{Lemma}{owner-as-dominator},
    we have that~$\hv'=\code{null} \text{~or~} \hl \Oprec \Owner{\hv'}$.

We assumed that~$K,\Gamma_{H} \vdash \hl.\hf_i = \code{\hv'} : \hT'$,
      therefore from \RULE{T-Field-Assignment}:
      \[
        K,\Gamma_{H} \vdash \hl.\hf_i : \hT
            \gap
        K,\Gamma_{H} \vdash \hl:\code{C<NO,NI>}
            \gap
        K,\Gamma_{H} \vdash \code{NI} \st \Raw
      \]
Similarly to field access, because~$K,\Gamma_{H} \vdash \hl.\hf_i : \hT$,
    then~$\hf_i \in \fields{}(\hC)$.
From our syntax~$\code{NI}$ is either \Mutable or $\Immut_{\hl'}$.
We want to show that~$\code{NI}=\Mutable \text{~or~} \Cooker{\hl} \in K$.
Therefore we need to show that if~$\code{NI}=\Immut_{\hl'}$ then~$\hl' \in K$.
Because~$K,\Gamma_{H} \vdash \code{NI} \st \Raw$, it must be from \RULE{S10} and therefore~$\hl' \in K$.

  \item[Rule~\RULE{R-Invoke}]
  \[
 \typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ldots}
    \gap
  \mbody{}(\hm,\code{C})=\ol{\hx}.\he'
}{
  K \vdash H,\hl\code{.m(}\ol{\hv}\code{)} \reducesto H, [\ol{\hv}/\ol{\hx}, \hl/\this, \hl/\This, \code{NO}/\hO, \code{NI}/\hI]\he'
}
    \]
  We assumed that~$K,\Gamma_{H} \vdash \hl\code{.m(}\ol{\hv}\code{)} : \hT"$,
    therefore from \RULE{T-Invoke} we know that \[
    \mtype{}(\hl,\hm,\code{C<NO,NI>})=\ol{\code{T}}\rightarrow\code{T"}
    \]
    Therefore~$\mbody{}(\hm,\code{C})$ is defined.

  \item[Rule~\RULE{R-New}]
  \[
  \typerule{
  \hl \not \in \dom(H)
    \gap
  \code{VI}' =
    \begin{cases}
    \Immut_\hl & \text{if~}\code{VI}=\Immut \text{~or~} (\code{VI}=\Immut_{\hc} \text{~and~} \hc \not \in K) \\
    \code{VI} & \text{otherwise} \\
    \end{cases}
    \gap
  H'=H[\hl \mapsto \code{C<NO,VI'>}\hparen{\ol{\code{null}}}]
}{
  K \vdash H,\code{new C<NO,VI>}\hparen{\ol{\hv}} \reducesto H',\hl\code{.build}\hparen{\ol{\hv}}\code{;return l}
}
    \]
    We assumed that~$K,\Gamma_{H} \vdash \code{new C<NO,VI>}\hparen{\ol{\hv}} : \hT"$,
        therefore from \RULE{T-New} we know that \[
          \mtype{}(\bot,\code{build},\code{C<NO,NI>})=\ol{\code{T}}\rightarrow\code{U}
          \]
    Thus there is a constructor with~$\#(\ol{\hv})$ of arguments.


  \item[Rule~\RULE{R-return}]
    Trivial because there are no assumptions for~\code{v;return l}
\end{description}

\end{proof}

We prove \textbf{preservation} (\Ref{Lemma}{part-subtype}) for method invocation
    by using \Ref{Lemma}{invoke-substitution} that uses
    induction on the size of the method body.

\begin{Lemma}[invoke-substitution]
  \textbf{(Invocation Substitution)}
    For every heap~$H$ that is well-typed for $K$,
        location~$\hl \in \dom(H)$, values~$\ol{\hv}$, types~$\code{U}$, and guard~\code{IG},
        where \beqs{invoke-substitution1}
            H[\hl] & = \code{C<NO,NI>}\\
            K,\Gamma_H & \vdash \code{NI} \st \code{IG}\\
            K,\Gamma_H & \vdash \ol{\hv} : \ol{\hU'}\\
            K,\Gamma_H & \vdash \ol{\hU'} \st \ol{[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{U}}\\
        \eeq
    Then, for any~$\he"$ such that
        $\emptyset,\Gamma \vdash \he":\hS$,~$\Gamma = \{ \hI:\code{IG}, \ol{\hx}:\ol{\code{U}},\this:\code{C<O,I>} \}$,
        then \beqst
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he" : \hS' \\
        K,\Gamma_H & \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS\\
        \eeq
\end{Lemma}
\begin{proof}

We will prove by induction on the structure of~$\he"$.

\begin{description}
  \item[$\he"=(\code{e;return l})$] Impossible because $\Gamma$ does not contain locations.
  \item[$\he"=(\hv)$] $\Gamma$ does not contain locations. Therefore,~$\hv=\code{null}$, and we can choose~$\hS' = [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS$.
  \item[$\he"=(\this)$] Then~$\hS = \code{C<O,I>}$,
    and
    \beqst
        & [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he" = \hl \\
        & [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS = \code{C<NO,NI>}\\
        & \hS' = \code{C<NO,NI>}\\
        & K,\Gamma_H \vdash \hl : \hS' \\
        & K,\Gamma_H \vdash \hS' \st \code{C<NO,NI>}\\
        \eeq

    \item[$\he"=(\hx_i)$] Then~$\hS = \hU_i$.
    We assumed that \beqst
        K,\Gamma_H & \vdash \hv_i : \hU'_i\\
        K,\Gamma_H & \vdash \hU'_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{U}_i\\
    \eeq
    Therefore,
    \beqst
        & [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he" = \hv_i \\
        & \hS' = \hU'_i\\
        & \hS = \hU_i\\
        & K,\Gamma_H \vdash \hv_i : \hS' \\
        & K,\Gamma_H \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS\\
        \eeq



  \item[$\he"=(\code{new D<FO,VI>}\hparen{\ol{\he}})$]
    We assumed that~$K,\Gamma_H \vdash \code{new D<FO,VI>}\hparen{\ol{\he}}:\hS$.
    From \RULE{T-new}, $\hS = \code{D<FO,VI>}$ and \beq{new0}
  \mtype{}(\bot,\code{build},\code{D<FO,VI>})=\ol{\code{T}}\rightarrow\code{U}
    \gap
  \emptyset,\Gamma \vdash \ol{\he}:\ol{\code{T}'}
    \gap
  \emptyset,\Gamma \vdash \ol{\code{T}'} \st \ol{\code{T}}
    \eeq
    By induction on~$\he_i$, we have that \beqs{new1}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he_i : \code{V}_i \\
        K,\Gamma_H & \vdash \code{V}_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{T}'_i\\
        \eeq
    From \Ref{Lemma}{subtyping-substitute} and~\eq{new0}, we have that \beq{new2}
        K,\Gamma_H \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{T}'_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{T}_i
    \eeq
    From transitivity,~\eq{new1}, and~\eq{new2}, we have \beq{new3}
        K,\Gamma_H \vdash \code{V}_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{T}_i
    \eeq
    From definition of $\mtype$ we have \beq{new4}
        \mtype{}(\bot,\code{build},[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<FO,VI>})=[\hl/\This,\code{NI}/\hI,\code{NO}/\hO](\ol{\code{T}}\rightarrow\code{U})
    \eeq
    From \RULE{T-new},~\eq{new3}, and~\eq{new4}, \beqst
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\code{new D<FO,VI>}\hparen{\ol{\he}} : [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<FO,VI>} \\
    \eeq

  \item[$\he"=(\code{e.f})$]
    From \RULE{T-Field-Access}, \beqst
        \emptyset,\Gamma &\vdash \he : \code{D<MO,IP>}\\
        \emptyset,\Gamma &\vdash \code{e.f} : \hS\\
        \hS &= \ftype(\he,\hf,\code{D<MO,IP>})\\
    \eeq
    Recall that~$\hS = \ftype{}(\he,\hf,\code{D<MO,IP>}) = \substitute(\he,\code{D<MO,IP>},\ftype{}(\hf,\code{D}))$.
    Note that~\he is not a location, and thus if \hf is \this-owned, then $\he=\this$.
    Consider first the case that \hf is \this-owned, thus $\he=\this$.
    Let~$\ftype{}(\hf,\code{D})=\code{FT}$, and~$\Ofn{\code{FT}}=\This$.
    We assumed that~$\emptyset,\Gamma \vdash \this.f:\hS$.
    Then,~$\hS=\code{FT}$.
    We need to show that
        \beqst
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\code{this.f} : \hS' \\
        K,\Gamma_H & \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}\\
        \eeq
    From \RULE{T-Field-Access} \[
        K,\Gamma_H \vdash \code{l.f} : [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}
    \], i.e., $\hS' = [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}$.

    Now suppose that \hf is not \this-owned.
    Therefore,~$\hS = [\code{IP}/\hI,\code{MO}/\hO]\code{FT}$.
    We need to show that
        \beqs{Access1}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\code{e.f} : \hS' \\
        K,\Gamma_H & \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS \gap \hS = [\code{IP}/\hI,\code{MO}/\hO]\code{FT}\\
        \eeq
    From the induction on~\he, we have that
        \beqs{Access2}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he : \hS" \\
        K,\Gamma_H & \vdash \hS" \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>}\\
        \eeq
    From~\eq{Access2},~$\Ofn{\hS"}=[\hl/\This,\code{NO}/\hO]\code{MO}$.
    From~\eq{Access1} and~\eq{Access2}, and \Ref{Lemma}{subtyping2}, we have that \beqst
        &\hS' = \ftype{}(\bot,\hf,\hS") = [\Ifn{\hS"}/\hI,\Ofn{\hS"}/\hO]\code{FT}
            \st [([\code{NI}/\hI]\code{IP})/\hI,([\hl/\This,\code{NO}/\hO]\code{MO})/\hO]\code{FT} =\\
            &= [\hl/\This,\code{NI}/\hI,\code{NO}/\hO] ([\code{IP}/\hI,\code{MO}/\hO]\code{FT})\\
    \eeq

  \item[$\he"=(\code{e.f=e}')$]
    The challenge in field assignment is that (by induction) the type of the substitution of~\he
        changed covariantly (i.e., it is a subtype of the substitution of the type),
        and $\he'$ also changed covariantly.
    However, we will prove that because $\Ifn{\he}$ is \Raw, and \he is either \this or \this-owned, then \he is invariant.

    We assumed that~$\emptyset,\Gamma \vdash \code{e.f=e}':\hS$.
    From \RULE{T-Field-Assignment}, we know that \beqs{assign0}
&\emptyset,\Gamma \vdash \he.\hf : \hT
    \gap
  \emptyset,\Gamma \vdash \he':\hS
    \gap
  \emptyset,\Gamma \vdash \hS \st \hT
    \gap
  \emptyset,\Gamma \vdash \he:\code{D<MO,IP>}
    \\
&  \emptyset,\Gamma \vdash \code{IP} \st \Raw
    \gap
  \isTransitive(\he,\Gamma,\code{D<MO,IP>})
    \gap
  \code{MO} \neq \code{?}\\
  \eeq
  We wish to prove all the assumptions in~\eq{assign0} after substituting~$[\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]$.



  By induction on~$\he'$ we have that
    \beqs{assign1}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he' : \hS' \\
        K,\Gamma_H & \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS\\
        \eeq
  By induction on~$\he.\hf$ we have that
    \beqs{assign2}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he.\hf : \hT' \\
        K,\Gamma_H & \vdash \hT' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT\\
        \eeq
  From the proof of field access above, we see that the class of~$\hT'$ and~\hT is the same.
  By induction on~$\he$ we have that
    \beqs{assign3}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he : \code{D'<MO',IP'>} \\
        K,\Gamma_H & \vdash \code{D'<MO',IP'>} \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>}\\
        \eeq
  Because~$\code{MO} \neq \code{?}$, from \Ref{Lemma}{Owners-Invariant} part (i), we have that~$\code{MO'}=\code{MO}$.

  We now prove that the following holds:
  \beqs{assign4}
  & K,\Gamma_H \vdash [\code{NI}/\hI]\code{IP} \st \Raw\\
  & \isTransitive([\hl/\this]\he,\Gamma,[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>})\\
    \eeq
  From~\eq{assign0},~$\emptyset,\Gamma \vdash \code{IP} \st \Raw$.
  From our syntax, and because~$\Gamma$ does not contain locations:\[
    \code{IP} = \ReadOnly ~|~ \Immut ~|~ \Mutable ~|~ \hI
  \]
  If~$\code{IP}=\Mutable$ then we proved~\eq{assign4}.
  Therefore, it must be that~$\code{IP}=\hI$ (thus~$[\code{NI}/\hI]\code{IP}=\code{NI}$)
    and~$\Gamma(\hI)=\code{IG} \st \Raw$.
  From~\eq{invoke-substitution1} ($K,\Gamma_H \vdash \code{NI} \st \code{IG}$),
    we proved the first part of~\eq{assign4} that~$K,\Gamma_H \vdash [\code{NI}/\hI]\code{IP} \st \Raw$.
  If~$\code{IG}=\Mutable$ then,
    $\code{NI}=\Mutable$, which proved~\eq{assign4}.
  Therefore~$\code{IG}=\Raw$, and from the definition of~$\isTransitive$ we have
    that~$\code{e=\this{}}\text{~or~~}\code{MO}=\This$.
  If~$\he=\this$ then~$\isTransitive(\hl,\ldots)$, which proved~\eq{assign4}.
  Thus~$\code{MO}=\This$, and
  \beqs{assign5}
    \code{D<MO,IP>} &= \code{D<This,I>}\\
    [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>} &= \code{D<\hl,\code{NI}>}\\
  \eeq
  From~\eq{invoke-substitution1},~$H[\hl] = \code{C<NO,NI>}$.
  If~$\code{NI}=\Mutable$ then we proved~\eq{assign4}.
  Otherwise~$\code{NI}=\Immut_{\hl'}$.
  Because $H$ is well-typed for $K$, $\hl' \Tprec \hl$, thus~$\hl' \not \OprecNotEqual \hl$,   proving~\eq{assign4}
    (because if~$\code{a} \OprecNotEqual \code{b}$ then~$\code{b} \TprecNotEqual \code{a}$).


  \textbf{(i)~}If~$\he=\this$.
    Let~$\ftype{}(\hf,\code{D})=\code{FT}$.
    We assumed in~\eq{assign0} that~$\emptyset,\Gamma \vdash \this.f:\hT$.
    Then,~$\hT=\code{FT}$.
    From \RULE{T-Field-Access} \[
        K,\Gamma_H \vdash \code{l.f} : [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}
    \]
    From definition of~$\isTransitive{}$, we have that~$\isTransitive{}(\hl,\ldots)$ holds.
    From \eq{assign0} ($\emptyset,\Gamma \vdash \hS \st \hT$) and \Ref{Lemma}{subtyping-substitute}, we have
    \beqs{this0}
        K,\Gamma_H \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT
    \eeq
    From \eq{assign1}, \eq{this0}, and transitivity, we have
    \beqs{this1}
    K,\Gamma_H & \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}
    \eeq
    To summarize, from \eq{this1}, \eq{assign4} ($K,\Gamma_H \vdash \code{NI} \st \Raw$), we have that
    \beqs{this2}
    &K,\Gamma_H \vdash \hl.\hf : [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}
        \gap
    K,\Gamma_H \vdash \he':\hS'
        \gap
    K,\Gamma_H \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}
        \\
    &K,\Gamma_H \vdash \hl:\code{C<NO,NI>}
        \gap
    K,\Gamma_H \vdash \code{NI} \st \Raw
        \gap
    \isTransitive(\hl,\ldots)
  \eeq
  Therefore, from~\eq{this2}, and \RULE{T-Field-Assignment}, we proved that \beqst
    K,\Gamma_H &\vdash \code{l.f=e}' : \hS' \\
    K,\Gamma_H &\vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{FT}\\
  \eeq


  \textbf{(ii)~}If $\he\neq\this$, then from~\eq{assign4}, we have
  \beqs{not-this1}
  & \isTransitive(\bot,\Gamma,[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>})\\
  \eeq
    From~\eq{assign3} and~\eq{not-this1} and \Ref{Lemma}{isTransitive}, we have that~$\code{IP'}=[\code{NI}/\hI]\code{IP}$.
  To summarize, from \eq{assign1}, \eq{assign2}, \eq{this0}, \eq{not-this1},
  \beqs{not-this2}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he.\hf : [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT \\
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he' : \hS' \\
        K,\Gamma_H & \vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS\\
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hS \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT\\
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he : \code{D'<MO,IP'>} \\
        K,\Gamma_H & \vdash \code{IP'} \st \Raw\\
        & \isTransitive(\bot,\Gamma,\code{D'<MO,IP'>})
    \gap
    \code{MO} \neq \code{?}\\
  \eeq
  Thus, from~\eq{not-this2}, and \RULE{T-Field-Assignment},  we proved that \beqst
    K,\Gamma_H &\vdash \code{e.f=e}' : \hS' \\
    K,\Gamma_H &\vdash \hS' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{S}\\
  \eeq


  \item[$\he"=(\he_0\code{.m}\hparen{\ol{\he}})$]
    The proof is similar in spirit to field assignment:
        the challenge is that both $\he_0$ and $\he_i$ change covariantly.
    Let~$\code{IG'}$ be the guard of \hm.
    If~$\code{IG'} = \ReadOnly$ then the parameters of \hm cannot include~\hI.
    If~$\code{IG'} = \Mutable ~|~ \Immut$, then~\hI remains with the same bound.
    The challenge is when~$\code{IG'} = \Raw$, then we use either the fact the~$\he_0$ is either \this or \this-owned,
        to prove that $\he_0$ is invariant (like in field assignment).

    With respect to wildcards, if the receiver $\he_0$ has a wildcard, then after the covariant change
        it might no longer be the case.
    Therefore we require that the owner of method parameters in this case must be \World.
        (it cannot be \hO nor \This).


    From \RULE{T-Invoke},
    \beq{invoke1}
    \typerule{
  \emptyset,\Gamma \vdash \he_0:\code{D<MO,IP>}
    \gap
  \mtype{}(\he_0,\hm,\code{D<MO,IP>})=\ol{\code{T}}\rightarrow\code{W}
    \gap
  \emptyset,\Gamma \vdash \ol{\he}:\ol{\code{T'}}
    \gap
  \emptyset,\Gamma \vdash \ol{\code{T'}} \st \ol{\code{T}}
    \gap
  \mguard{}(\hm,\code{D})=\code{IG'}
    \\
  \emptyset,\Gamma \vdash \code{IP} \st \code{IG'}
    \gap
  \code{IG'}=\Raw \Rightarrow \isTransitive(\he_0,\Gamma,\code{D<MO,IP>})
    \gap
  \mtype{}(\hm,\code{D})=\ol{\code{U}}\rightarrow\code{V}
    \gap
  \Ofn{\ol{\code{T}}}=\code{?} \Rightarrow \Ofn{\ol{\code{U}}}=\code{?}
}{
  \emptyset,\Gamma \vdash \he_0\code{.m(}\ol{\he}\code{)} : \code{W}
}
\eeq

By induction on~$\he_0$, we have that
    \beqs{invoke3}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he_0 : \code{D'<MO',IP'>} \\
        K,\Gamma_H & \vdash \code{D'<MO',IP'>} \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>}\\
        \eeq
Note that, in contrast with field assignment, here we might have~$\code{MO}=\code{?}$, and then~$\code{MO'}\neq\code{MO}$.
However, from \Ref{Lemma}{Owners-Invariant} part (i),
\beq{invoke-owner-wildcard}
    \code{MO}\neq\code{?} \Rightarrow \code{MO'}=[\hl/\This,\code{NO}/\hO]\code{MO}
\eeq

By induction on~$\he_i$, we have that
    \beqs{invoke4}
        K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he_i : \hS_i' \\
        K,\Gamma_H & \vdash \hS'_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{T'}_i\\
        \eeq
From~\eq{invoke4} and~\eq{invoke1} and \Ref{Lemma}{subtyping-substitute}, we have
    \beqs{invoke5}
        &K,\Gamma_H \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{T'}_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT_i\\
    \eeq
From transitivity,~\eq{invoke4}, and~\eq{invoke5},
    \beqs{invoke6}
        &K,\Gamma_H \vdash \hS'_i \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT_i\\
    \eeq


Because method overriding maintains the same signature,
    we have that
\beqs{invoke-signature1}
\mtype{}(\hm,\code{D'})=\mtype{}(\hm,\code{D})=\ol{\code{U}}\rightarrow\code{V}
\eeq
From definition of $\mtype$, \eq{invoke-signature1}, and because~$\he_0$ does not contain locations, we have that
\beqs{invoke-signature2}
\mtype{}(\he_0,\hm,\code{D<MO,IP>})=\ol{\code{T}}\rightarrow\code{W}=[\code{MO}/\hO, \code{IP}/\hI](\ol{\code{U}}\rightarrow\code{V})\\
\mtype{}([\hl/\this]\he_0,\hm,\code{D'<MO',IP'>})=[\hl/\This,\code{MO'}/\hO, \code{IP'}/\hI](\ol{\code{U}}\rightarrow\code{V})\\
\eeq
We will always prove that the parameters are invariant, i.e.,
\beq{invoke-signature-to-prove}
\mtype{}([\hl/\this]\he_0,\hm,\code{D'<MO',IP'>})=\ol{[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\hT_i}\rightarrow\code{W'}
\eeq
We will also prove that
\beq{invoke-to-prove}
    K,\Gamma_H \vdash \code{IP'} \st \code{IG'}
    \gap
  \code{IG'}=\Raw \Rightarrow \isTransitive([\hl/\this]\he_0,\Gamma,\code{D'<MO',IP'>})
\eeq
Because there are no wildcards after substitution, from~\eq{invoke-signature-to-prove} and~\eq{invoke-to-prove},
    we will have that
    \beqst
    K,\Gamma_H & \vdash [\hl/\This,\code{NI}/\hI,\code{NO}/\hO, \ol{\hv}/\ol{\hx}, \hl/\this]\he_0\code{.m(}\ol{\he}\code{)} : \code{W}' \\
    K,\Gamma_H & \vdash \code{W}' \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{W}\\
    \eeq


Next we prove~\eq{invoke-signature-to-prove} just for the owner parameter, i.e., we want to show that (from~\eq{invoke-signature2} and~\eq{invoke-signature-to-prove})
\beq{invoke-owner0}
    \Ofn{[\hl/\This,\code{MO'}/\hO]\code{U}_i} = \Ofn{[\hl/\This,\code{NO}/\hO]\hT_i}
\eeq
From~\eq{invoke-signature2},
\beq{invoke-owner1}
    \Ofn{\hT_i}=\Ofn{[\code{MO}/\hO]\code{U}_i}
\eeq
If~$\Ofn{\code{U}_i}=\This$, then both sides of \eq{invoke-owner0} are~\hl.
If~$\Ofn{\code{U}_i}\neq\hO$, then both sides of \eq{invoke-owner0} are~$\Ofn{\code{U}_i}$.
The last case is that~$\Ofn{\code{U}_i}=\hO$.
From~\eq{invoke1}, we have
\beq{invoke-owner2}
    \Ofn{\code{T}_i}=\code{?} \Rightarrow \Ofn{\code{U}_i}=\code{?}
\eeq
On the one hand, if~$\code{MO}=\code{?}$, then~$\Ofn{\code{T}_i}=\code{?}$, thus~$\Ofn{\code{U}_i}=\code{?}$,
    and both sides of \eq{invoke-owner0} are~$\code{?}$.
On the other hand, if~$\code{MO}\neq\code{?}$, then from \eq{invoke-owner-wildcard} %\code{MO}\neq\code{?} \Rightarrow \code{MO'}=[\hl/\This,\code{NO}/\hO]\code{MO}$.
    \[
    \code{MO'}=[\hl/\This,\code{NO}/\hO]\code{MO}
    \]
which proves~\eq{invoke-owner0}.

From \eq{invoke-owner0},
    in order to prove~\eq{invoke-signature-to-prove}, we just need to show it for the immutability parameter,
    i.e., (from \eq{invoke-signature2})
\beq{invoke-immutability}
\Ifn{[\code{IP'}/\hI]\code{U}_i}=\Ifn{[\code{NI}/\hI]([\code{IP}/\hI]\code{U}_i)}
\eeq
Recall the following:
From~\eq{invoke3}, we know that
        $K,\Gamma_H \vdash \code{D'<MO',IP'>} \st [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>}$.
From~\eq{invoke1},~$\emptyset,\Gamma \vdash \code{IP} \st \code{IG'}$.
From~\eq{invoke-substitution1},~$K,\Gamma_H \vdash \code{NI} \st \code{IG}$
    and $\hI:\code{IG} \in \Gamma$.

We will split the proof by the four possible values of $\code{IG'} = \ReadOnly ~|~ \Mutable ~|~ \Immut ~|~ \Raw$.
For each case we need to prove~\eq{invoke-to-prove} and~\eq{invoke-immutability}.
%K,\Gamma_H \vdash \code{IP'} \st \code{IG'}
%    \gap
%  \code{IG'}=\Raw \Rightarrow \isTransitive([\hl/\this]\he_0,\Gamma,\code{D'<MO',IP'>})

\textbf{(i) $\code{IG'} =\ReadOnly$}
Because any immutability is a subtype of \ReadOnly, we proved \eq{invoke-to-prove}.
Furthermore, when $\code{IG'} =\ReadOnly$ the signature of parameters cannot contain~\hI,
    i.e., $\Ifn{\code{U}_i}\neq\hI$, which proved~\eq{invoke-immutability}.

\textbf{(ii) $\code{IG'} =\Mutable$}
From~\eq{invoke1},~$\emptyset,\Gamma \vdash \code{IP} \st \Mutable$,
    thus either $\code{IP}=\Mutable$ or~($\code{IG}=\Mutable$ and~$\code{IP}=\hI$).
If $\code{IP}=\hI$, then from~\eq{invoke-substitution1},~$K,\Gamma_H \vdash \code{NI} \st \Mutable$, thus~$\code{NI} = \Mutable$.
Thus,~$K,\Gamma_H \vdash [\code{NI}/\hI]\code{IP} \st \Mutable$.
Therefore, from~\eq{invoke3} and \Ref{Lemma}{Guard} part (i), we have that~$K,\Gamma_H \vdash \code{IP'} \st \Mutable$,
    which proved \eq{invoke-to-prove}.

We showed that if $\code{IP}=\hI$, then~$\code{NI} = \Mutable$ and~$\code{IP'}=\Mutable$, proving~\eq{invoke-immutability}.
We also showed that if $\code{IP}=\Mutable$ then~$\code{IP'}=\Mutable$, proving~\eq{invoke-immutability}.


\textbf{(iii) $\code{IG'} =\Immut$}
Exactly like part (ii), but we use \Ref{Lemma}{Guard} part (ii) instead of part (i),
    and ($\Immut_{\hl'}$ where~$\hl' \not\in K$) instead of \Mutable.

\textbf{(iv) $\code{IG'} =\Raw$}
Exactly like in field assignment, we prove that:
\beqs{invoke2}
  & K,\Gamma_H \vdash [\code{NI}/\hI]\code{IP} \st \Raw\\
  & \isTransitive([\hl/\this]\he,\Gamma,[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>})\\
\eeq

If $\he=\this$, then $\code{D}=\hC$, $\code{IP}=\hI$ (because~$\emptyset,\Gamma \vdash \this:\code{D<O,I>}$)
    and~$\code{IP'} = \code{NI}$ (because~$K,\Gamma_H \vdash \hl:\code{D<NO,NI>}$),
    therefore, \[
\Ifn{[\code{NI}/\hI]\code{U}_i}=\Ifn{[\code{NI}/\hI]([\hI/\hI]\code{U}_i)}
\]
which proved \eq{invoke-immutability}.
Furthermore, because~$\emptyset,\Gamma \vdash \code{IP} \st \Raw$ (and~$\code{IP}=\hI$),
    we know that~$\code{IG} \st \Raw$.
Thus from~\eq{invoke-substitution1},~$K,\Gamma_H \vdash \code{NI} \st \Raw$.
Finally because \this was replaced with \hl, and $\isTransitive(\hl,\ldots)$ always holds,
    then we proved \eq{invoke-to-prove}.

If $\he\neq\this$, then from \eq{invoke2}, we have that
    $\isTransitive(\bot,\Gamma,[\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>})$,
    thus from definition of $\isTransitive$ we have that~$\code{MO}\neq\code{?}$.
From \Ref{Lemma}{Guard} part (iii) and~\eq{invoke3}, we know that
        $\code{IP'} = [\code{NI}/\hI]\code{IP}$,
        which proved~\eq{invoke-immutability}.
Combined with~\eq{invoke2}, we have that~$K,\Gamma_H \vdash \code{IP'} \st \Raw$.
From \eq{invoke-owner-wildcard}, we have~$\code{MO'}=[\hl/\This,\code{NO}/\hO]\code{MO}$.
Therefore,~$\code{D'<MO',IP'>} = [\hl/\This,\code{NI}/\hI,\code{NO}/\hO]\code{D<MO,IP>}$,
    which proved \eq{invoke-to-prove}.
\end{description}

\end{proof}


\begin{Lemma}[part-subtype]
  \textbf{(Subtype preservation)}
    For every closed expression~$\he" \neq \hv$, $H$, and $K$,
        if $K,\Gamma_{H} \vdash \he" : \hT"$
        and~$K \vdash H,\he" \reducesto H',\grave{\he}$
        and $H$ is well-typed for $K \cup K(\he")$,
        then
        $K,\Gamma_{H'} \vdash \grave{\he}:\grave{\hT}$
        and~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.
\end{Lemma}
\begin{proof}
We prove by examining all possible reduction rules.
\begin{description}
  \item[Congruence for field access]
Consider the congruence rule for field access \[
    \typerule{
    K \vdash H,\he \reducesto H',\he'}
    {
    K \vdash H,\he.\hf \reducesto H',\he'.\hf}
\]
We assumed that $K,\Gamma_{H} \vdash \he.\hf : \hT"$ and
    by induction~$K,\Gamma_{H} \vdash \he:\hT$,~$K,\Gamma_{H'} \vdash \he':\hT'$ and~$K,\Gamma_{H'} \vdash \hT' \st \hT$.
Let~$\hT = \code{C<MO,IP>}$.
Because $\he \neq \this$ (cause \he is closed) and~$\he \neq \hl$ (cause a location cannot be reduced further),
    then field~$\hf$ is not \this-owned,
    and~$\hT" = \ftype{}(\bot,\hf,\hT)$.

Because~$K,\Gamma_{H'} \vdash \hT' \st \hT$,
    from \Ref{Lemma}{Owners-Invariant} part (iii),
    then~\code{C'} is a subtype of \code{C}.
Therefore $\fields(\code{C'})$ must contain the same field~$\hf$ which is not \this-owned.
Thus,~$K,\Gamma_{H'} \vdash \grave{\he}:\grave{\hT}$,
    where~$\grave{\hT} = \ftype{}(\bot,\hf,\hT')$.
The last thing we need to prove is that~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$,
    which follows from \Ref{Lemma}{subtyping-substitute2}.

  \item[Congruence for method receiver]
Consider the congruence rule for method receiver \[
    \typerule{
    K \vdash H,\he_0 \reducesto H',\he'_0}{
    K \vdash H,\he_0\code{.m}\hparen{\ol{\he}} \reducesto H',\he'_0\code{.m}\hparen{\ol{\he}}}
\]
Similarly to field access, because~$\he_0$ is not a location,
    then none of the parameters or return type of method~\hm is \this-owned.
Proving that~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$
    (i.e., the return type is preserved)
    is done similarly to field access,
    by noting that method overriding maintains the same return type.
    (The return type could also change covariantly and the proof would still hold.)
However, proving that~$K,\Gamma_{H'} \vdash \grave{\he}:\grave{\hT}$ is more challenging
    because:
    (i)~we need to show that~$\he'_0$ satisfies the guard, and
    (ii)~the type of method parameters after substitution can change covariantly (as opposed to FGJ, which is invariant).


We will first prove that~$\he'_0$ satisfies the guard.
We assumed that $K,\Gamma_{H} \vdash \he_0\code{.m}\hparen{\ol{\he}} : \hT"$ and
    by induction~$K,\Gamma_{H} \vdash \he_0:\hT$,~$K,\Gamma_{H'} \vdash \he'_0:\hT'$ and~$K,\Gamma_{H'} \vdash \hT' \st \hT$.
From \RULE{T-Invoke},
    we know that \[
  K,\Gamma_H \vdash \he_0:\code{C<MO,IP>}
    \gap
  \mguard{}(\hm,\code{C})=\code{IG}
    \gap
  K,\Gamma_H \vdash \code{IP} \st \code{IG}
    \gap
  \code{IG}=\Raw \Rightarrow \isTransitive(\he_0,\Gamma,\code{C<MO,IP>})
    \]
Because~$\he_0$ is neither \this nor \hl (because it was reduced),
    then~$\code{IG}=\Raw \Rightarrow \isTransitive(\bot,\Gamma,\code{C<MO,IP>})$.
Let~$\hT' = \code{C'<MO,IP'>}$ and~$\mguard{}(\hm,\code{C'})=\code{IG'}$.
Because~$K,\Gamma_{H'} \vdash \hT' \st \hT$,
    from \Ref{Lemma}{Owners-Invariant} part (iii),
    then~\code{C'} is a subtype of \code{C}.
From the restriction on method overriding with guards,~$\code{IG} \st \code{IG'}$.
From \Ref{Lemma}{Guard} part (iv),
    we have that~$\code{IP'} \st \code{IG}$.
From transitivity,~$\code{IP'} \st \code{IG'}$.

Next we show that~$\code{IG}=\Raw \Rightarrow \isTransitive(\he'_0,\Gamma,\code{C'<MO,IP'>})$.
If~$\code{IG}=\Raw$ then we showed that~$\isTransitive(\bot,\Gamma,\code{C<MO,IP>})$.
From \Ref{Lemma}{isTransitive} we have that~$\code{IP'}=\code{IP}$,
    thus~$\code{IG}=\Raw \Rightarrow \isTransitive(\he'_0,\Gamma,\code{C'<MO,IP'>})$.

Let
\beqst
\mtype{}(\he_0,\hm,\code{C<MO,IP>})=\ol{\code{U}}\rightarrow\code{V} \\
\mtype{}(\he'_0,\hm,\code{C'<MO,IP'>})=\ol{\code{U'}}\rightarrow\code{V'} \\
K,\Gamma_H \vdash \ol{\he}:\ol{\code{U"}}\\
\eeq
Because~$K,\Gamma_H \vdash \ol{\code{U"}} \st \ol{\code{U}}$,
    from \Ref{Lemma}{invokeSubtype}, we have that~$K,\Gamma_H \vdash \ol{\code{U"}} \st \ol{\code{U'}}$.

Therefore, all the assumptions in \RULE{T-Invoke} are fulfilled (the requirement for wildcards is fulfilled because all types are closed),
    and we proved that~$K,\Gamma_{H'} \vdash \grave{\he}:\grave{\hT}$.


  \item[Congruence for method argument]
    Trivial.

  \item[Congruence for new instance]
    Trivial.

  \item[Congruence for the rvalue of field assignment]
    Trivial.

  \item[Congruence for the receiver of field assignment]
Consider the congruence rule for the receiver of field assignment \[
    \typerule{
    K \vdash H,\he \reducesto H',\he'}{
    K \vdash H,\code{e.f=e"} \reducesto H',\code{e'.f=e"}}
\]
We assumed that $K,\Gamma_{H} \vdash \code{e.f=e"} : \hT"$ and
    by induction~$K,\Gamma_{H} \vdash \he:\hT$,~$K,\Gamma_{H'} \vdash \he':\hT'$ and~$K,\Gamma_{H'} \vdash \hT' \st \hT$.
We will show that~$K,\Gamma_{H} \vdash \code{e.f=e"} : \hT"$.
From \RULE{T-Field-Assignment}:
\[
  K,\Gamma_H \vdash \he.\hf : \code{F}
    \gap
  K,\Gamma_H \vdash \code{e"}:\code{T"}
    \gap
  K,\Gamma_H \vdash \code{T"} \st \code{F}
    \gap
  K,\Gamma_H \vdash \he:\code{C<MO,IP>}
    \gap
  K,\Gamma_H \vdash \code{IP} \st \Raw
    \gap
  \isTransitive(\he,\Gamma_H,\code{C<MO,IP>})
\]
We need to show that:
\[
  K,\Gamma_H \vdash \he'.\hf : \code{F'}
    \gap
  K,\Gamma_H \vdash \code{T"} \st \code{F'}
    \gap
  K,\Gamma_H \vdash \he':\code{C'<MO,IP'>}
    \gap
  K,\Gamma_H \vdash \code{IP'} \st \Raw
    \gap
  \isTransitive(\he,\Gamma_H,\code{C'<MO,IP'>})
\]
Because \he was reduced, we know it is not a location, so~$\isTransitive(\bot,\Gamma_H,\code{C<MO,IP>})$.
From \Ref{Lemma}{isTransitive}, we have that~$\code{IP}=\code{IP'}$.
Therefore~$\code{F'}=\code{F}$ (because $\ftype(\hf,\hC)=\ftype(\hf,\hC')$),
    and~$\isTransitive(\he,\Gamma_H,\code{C'<MO,IP'>})$.



  \item[Congruence for return~\RULE{R-c1}]
Consider the congruence rule for \code{e;return l} \[
\typerule{
  K \cup \{\hl\} \vdash H,\he \reducesto H',\he'
}{
  K \vdash H,\code{e;return l} \reducesto H',\code{e';return l}
}
\]
We assumed that \beqst
    K,\Gamma_{H} \vdash \code{e;return l} : \hT"
    \gap
    \he"=\code{e;return l}
    \gap
    \grave{\he}=\code{e';return l}
    \\
    K \cup \{\hl\},\Gamma_{H} \vdash \he:\hT
    \gap
    K \cup \{\hl\},\Gamma_{H'} \vdash \he':\hT'
    \gap
    K \cup \{\hl\},\Gamma_{H'} \vdash \hT' \st \hT
    \eeq
We need to prove that~$K,\Gamma_{H'} \vdash \grave{\he} :\grave{\hT}$ and~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.

According to \RULE{T-return}:
\[
\typerule{
  K \cup \{ \hl \},\Gamma_{H'} \vdash \he':\hT'
}{
  K,\Gamma_{H'} \vdash \code{e';return l} : \Gamma_{H'}(\hl)
}
\]
Because~$K \cup \{ \hl \},\Gamma_{\grave{H}} \vdash \he':\hT'$, we proved that~$K,\Gamma_{H'} \vdash \code{e';return l} : \Gamma_{H'}(\hl)$,
    i.e.,~$K,\Gamma_{H'} \vdash \grave{\he} :\grave{\hT}$.

We still need to prove that~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.
Because~$\grave{\hT}=\Gamma_{H'}(\hl)$ and~$\hT" = \Gamma_{H}(\hl)$
    then~$\grave{\hT}=\hT"$, and from reflexivity (\RULE{S2}) we have~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.


  \item[Rule~\RULE{R-return}] Trivial

  \item[Rule~\RULE{R-New}]
  According to \RULE{R-New} \[
\typerule{
  \hl \not \in \dom(H)
    \gap
  \code{VI}' =
    \begin{cases}
    \Immut_\hl & \text{if~}\code{VI}=\Immut \text{~or~} (\code{VI}=\Immut_{\hc} \text{~and~} \hc \not \in K) \\
    \code{VI} & \text{otherwise} \\
    \end{cases}
    \gap
  H'=H[\hl \mapsto \code{C<NO,VI'>}\hparen{\ol{\code{null}}}]
}{
  K \vdash H,\code{new C<NO,VI>}\hparen{\ol{\hv}} \reducesto H',\hl\code{.build}\hparen{\ol{\hv}}\code{;return l}
}
\]
We assumed that \[
    K,\Gamma_{H} \vdash \he" : \hT"
    \gap
    \he"=\code{new C<NO,VI>}\hparen{\ol{\hv}}
    \gap
    \grave{\he}=\hl\code{.build}\hparen{\ol{\hv}}\code{;return l}
    \]
We need to prove that~$K,\Gamma_{H'} \vdash \grave{\he} :\grave{\hT}$ and~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.

From \RULE{T-New}
\beq{R-new1}
\typerule{
  \mtype{}(\bot,\code{build},\code{C<NO,VI>})=\ol{\code{U}}\rightarrow\code{Z}
    \gap
  K,\Gamma_{H} \vdash \ol{\hv}:\ol{\code{V}}
    \gap
  K,\Gamma_{H} \vdash \ol{\code{V}} \st \ol{\code{U}}
}{
  K,\Gamma_{H} \vdash \code{new C<NO,VI>(}\ol{\hv}\code{)} : \code{C<NO,VI>}
}
\eeq
Thus,~$\hT" = \code{C<NO,VI>}$.
From~\RULE{T-return},~$\grave{\hT} = \code{C<NO,VI'>}$.
Because~$\hl \not \in K$, then~$K,\Gamma_{H'} \vdash \Immut_\hl \st \Immut$,
    thus~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.

We still need to prove that~$K,\Gamma_{H'} \vdash \grave{\he} :\grave{\hT}$,
    and from~\RULE{T-return} we need to prove that \[
    K \cup \{ \hl \},\Gamma_{H'} \vdash \hl\code{.build}\hparen{\ol{\hv}}:\code{Z}
    \]
Because~\hl is a new location, all the equations in~\eq{R-new1} are still true
    if we replace~$\Gamma_{H}$ with~$\Gamma_{H'}$.
From \RULE{T-invoke}, and because the guard of \code{build} is \Raw:
\[
\typerule{
  K \cup \{ \hl \},\Gamma_{H'} \vdash \hl:\grave{\hT}
    \gap
  \mtype{}(\hl,\code{build},\grave{\hT})=\ol{\code{W}}\rightarrow\code{Z'}
    \gap
  K \cup \{ \hl \},\Gamma_{H'} \vdash \ol{\hv}:\ol{\code{V}}
    \gap
  K \cup \{ \hl \},\Gamma_{H'} \vdash \ol{\code{V}} \st \ol{\code{W}}
    \\
  K \cup \{ \hl \},\Gamma_{H'} \vdash \code{VI'} \st \Raw
    \gap
  \isTransitive(\hl,\Gamma,\grave{\hT})
}{
  K \cup \{ \hl \},\Gamma_{H'} \vdash \hl\code{.build}\hparen{\ol{\hv}}:\code{Z'}
}
\]
Assumption~$\isTransitive(\hl,\Gamma,\grave{\hT})$ holds because~\hl is a location.
Because~$\hl \in K \cup \{ \hl \}$ and \code{VI} is either \Mutable or \Immut or $\Immut_{\hl'}$,
    then this assumption holds~$K \cup \{ \hl \},\Gamma_{H'} \vdash \code{VI'} \st \Raw$.
The only assumption left to prove is that~$K \cup \{ \hl \},\Gamma_{H'} \vdash \ol{\code{V}} \st \ol{\code{W}}$.
From~\eq{R-new1} we have that~$K \cup \{ \hl \},\Gamma_{H'} \vdash \ol{\code{V}} \st \ol{\code{U}}$.
If $\code{VI}=\Mutable$ then~$\ol{\code{U}}=\ol{\code{W}}$.
Otherwise $\code{VI}=\Immut$, ~$\grave{\hT} = \code{C<NO,\Immut}_\hl\code{VI>}$,
    and we have that
\beqst
&    \mtype{}(\code{build},\hC) = \ol{\code{FT}}\rightarrow\code{Z"}\\
&  \mtype{}(\hl,\code{build},\code{C<NO,\Immut}_\hl\code{VI>})=\ol{\code{W}}\rightarrow\code{Z'}\\
&  \mtype{}(\bot,\code{build},\code{C<NO,\Immut>})=\ol{\code{U}}\rightarrow\code{Z}\\
&    \code{W}_i = [\code{NO}/\hO,\Immut_\hl/\hI]\code{FT}_i\\
&    \code{U}_i = [\code{NO}/\hO,\Immut/\hI]\code{FT}_i\\
&    K \cup \{ \hl \},\Gamma_{H'} \vdash \code{V}_i \st \code{U}_i\\
\eeq
We want to prove that~$K \cup \{ \hl \},\Gamma_{H'} \vdash \code{V}_i \st \code{W}_i$.
If~$\Ifn{\code{FT}_i}\neq\hI$ then~$\code{W}_i=\code{U}_i$.
Because~$\Ofn{\code{FT}_i}\neq\This$, then it is either \hO or \World,
    thus,~$\Owner{\code{W}_i}$ is either \code{NO} or \World.
Finally note that~$\hl \OprecNotEqual \code{NO}$ (because~$\hl \mapsto \code{C<NO,\ldots>}$),
    and we always have that~$\code{NO} \Oprec \World$, thus~$\hl \OprecNotEqual \World$.
According to subtyping rule~\RULE{S13}, we have that~$K \cup \{ \hl \},\Gamma_{H'} \vdash  \code{U}_i \st \code{W}_i$,
    and from transitivity~$\code{V}_i \st \code{U}_i \st \code{W}_i$.


  \item[Rule~\RULE{R-Field-Access}]
  According to \RULE{R-Field-Access} \[
\typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ol{\hv}}
    \gap
  \fields{}(\hC)=\ol{\hf}
}{
  K \vdash H,\hl.\hf_i \reducesto H,\hv_i
}
\]
We assumed that~$K,\Gamma_{H} \vdash \hl.\hf_i : \hT"$, and
    we need to prove that~$K,\Gamma_{H} \vdash \hv_i :\grave{\hT}$ and~$K,\Gamma_{H} \vdash \grave{\hT} \st \hT"$.
If~$\hv_i=\code{null}$ then we can choose~$\grave{\hT} = \hT"$,
otherwise~$\hv_i\neq\code{null}$, and because the heap is well-typed for $K$, then~$K,\Gamma_{H} \vdash \grave{\hT} \st \hT"$.

  \item[Rule~\RULE{R-Field-Assignment}]
  According to \RULE{R-Field-Assignment} \[
\typerule{
  \ldots
}{
  K \vdash H,\hl.\hf_i = \code{\hv'} \reducesto H',\hv'
}
\]
We assumed that~$K,\Gamma_{H} \vdash \hl.\hf_i = \code{\hv'} : \hT"$, and
    we need to prove that~$K,\Gamma_{H'} \vdash \hv' :\grave{\hT}$ and~$K,\Gamma_{H'} \vdash \grave{\hT} \st \hT"$.
Because we did not add any new locations, we have~$\Gamma_{H} = \Gamma_{H'}$.
From \RULE{T-Field-Assignment}, we have that~$K,\Gamma_{H} \vdash \code{\hv'} : \hT"$, i.e.,~$\grave{\hT} = \hT"$.


  \item[Rule~\RULE{R-Invoke}]
According to \RULE{R-Invoke} \beqst
\typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ldots}
    \gap
  \mbody{}(\hm,\code{C})=\ol{\hx}.\he'
}{
  K \vdash H,\hl\code{.m(}\ol{\hv}\code{)} \reducesto H, [\ol{\hv}/\ol{\hx}, \hl/\this, \hl/\This, \code{NO}/\hO, \code{NI}/\hI]\he'
}
\eeq
We assumed that \beqst
    K,\Gamma_{H} \vdash \he" : \hT"
    \gap
    \he"=\hl\code{.m(}\ol{\hv}\code{)}
    \gap
    \grave{\he}=[\ol{\hv}/\ol{\hx}, \hl/\this, \hl/\This, \code{NO}/\hO, \code{NI}/\hI]\he'
    \eeq
From \RULE{T-Invoke} we have that \beqst
  \mtype{}(\hl,\hm,\code{C<NO,NI>})=\ol{\hT}\rightarrow\hT"
    \gap
  K,\Gamma_{H} \vdash \ol{\hv}:\ol{\hT'}
    \gap
  K,\Gamma_{H} \vdash \ol{\hT'} \st \ol{\hT}
    \gap
  \mguard{}(\hm,\code{C})=\code{IG}
    \gap
  K,\Gamma_{H} \vdash \code{NI} \st \code{IG}
\eeq
We know the method~\hm was typed-checked in~\hC, i.e.,
\beqst
 \Gamma & =\{\hI:\code{IG}, \ol{\hx}:\ol{\code{U}}, \this:\code{C<O,I>}\} \\
 \mtype(\hm,\code{C}) & =\ol{\code{U}}\rightarrow\code{FT} \\
 \emptyset,\Gamma &\vdash \he':\code{S} \\
 \emptyset,\Gamma &\vdash \code{S} \st \code{FT}\\
\eeq
From the definition of \mtype:
\beqst
 \mtype{}(\hl,\hm,\code{C<NO,NI>})&=\substitute{}(\hl,\code{C<NO,NI>},\mtype(\hm,\code{C})) \\
 \hT" &=  [\code{NO}/\hO,\code{NI}/\hI,\hl/\This]\code{FT}\\
 \hT_i &=  [\code{NO}/\hO,\code{NI}/\hI,\hl/\This]\code{U}_i\\
\eeq

We need to prove that~$K,\Gamma_{H} \vdash \grave{\he} :\grave{\hT}$ and~$K,\Gamma_{H} \vdash \grave{\hT} \st \hT"$,
    which follows immediately from \Ref{Lemma}{invoke-substitution}.
\end{description}
\end{proof}




\begin{Lemma}[part-well-typed]
  \textbf{(Well-typed heap preservation)}
    For every closed expression~$\he" \neq \hv$, $K$, and $H$,
        if $K,\Gamma_{H} \vdash \he" : \hT"$
        and~$K \vdash H,\he" \reducesto H',\grave{\he}$
        and $H$ is well-typed for $K \cup K(\he")$,
        then
        $H'$ is well-typed for~$K \cup K(\grave{\he})$.
\end{Lemma}
\begin{proof}
Recall that a {well-typed} heap~$H$ satisfies:
    (i)~there is a linear order~$\Tprec$ over~$\dom{}(H)$ such that for every location~\hl,
        $\Owner{\hl}=\World$ or $\Owner{\hl} \TprecNotEqual \hl$, and $\Ifn{\hl}=\Mutable$ or $\Cooker{\hl} \Tprec \hl$,
        and
    (ii)~each non-null field location is a subtype of the declared field type.
Recall also that from the definition of a heap~$H$, every location~\hl in~$H$ has the form:
    (iii)~$\hl \mapsto \hC\code{<\underline{NO,NI}>}\hparen{\ol{\hv}}$.

Consider the congruence rules, such as \[
    \typerule{
    K \vdash H,\he \reducesto H',\he'}{
    K \vdash H,\he.f \reducesto H',\he'.f}
\]
By the induction hypothesis~$H'$ is well-typed~$K \cup K(\grave{\he})$.

The only rule that changes~$K$ is \RULE{R-c1}:
\[
\typerule{
  K \cup \{\hl\} \vdash H',\he \reducesto H",\code{e'}
}{
  K \vdash H,\code{e;return l} \reducesto H",\code{e';return l}
}
\]
By induction~$H"$ is well-typed for~$(K \cup \{\hl\}) \cup K(\code{e'})$.
We need to prove that~$H"$ is well-typed for~$K \cup K(\code{e';return l})$.
By definition of $K(\ldots)$, we have that~$K \cup K(\code{e';return l}) = K \cup \{\hl\} \cup K(\code{e'})$.

Rules \RULE{R-Field-Access} and \RULE{R-Invoke} do not change the heap.

Rule \RULE{R-return} does not change the heap nor~$K$,
    however~$K(\grave{\he}) = K(\he") \setminus \{ \hl \}$,
According to \Ref{Lemma}{well-typed}, the resulting heap~$H'$
    is well-typed for~$K \cup K(\grave{\he})$.

Rule \RULE{R-New} creates a new object with \code{null} fields:
    \[
    \code{VI}' =
    \begin{cases}
    \Immut_\hl & \text{if~}\code{VI}=\Immut \text{~or~} (\code{VI}=\Immut_{\hc} \text{~and~} \hc \not \in K) \\
    \code{VI} & \text{otherwise} \\
    \end{cases}
        \gap
    \hl \not \in \dom(H)
        \gap
    H' = H[\hl \mapsto \code{C<NO,VI'>}\hparen{\ol{\code{null}}}]
    \]
The fields of the new object are all \code{null}, thus fulfilling demand (ii).

We extend the linear order~$\Tprec$ by adding the new location~\hl at the end.
Its owner~\code{NO} is either \World or an existing object~$\hl'$,
    and either $\code{VI}=\Mutable$ or $\code{VI}=\Immut_{\hl'}$
    (where~$\hl'$ is either an existing location or \hl),
    thus fulfilling demand (i).

Note that~$\he" = \code{new C<\underline{NO,VI}>}\hparen{\ol{\hv}}$, and because~$\he"$ is closed,
    then we have that~$\code{NO}$ and~$\code{VI}$ do not contain~\hO, \hI, nor~\This.
And if~$\code{VI}=\Immut$ then it is substituted with~$\Immut_\hl$, thus fulfilling demand (iii).
Finally, note that~$\grave{\he}=(\hl\code{.build}\hparen{\ol{\hv}}\code{;return l})$,
    i.e.,~$K(\grave{\he}) = K(\he") \cup \{ \hl \}$.
However, because~\hl is a \emph{new} location, it does not change existing subtype relations (it does not affect existing objects
    that do not refer to~\hl).
Therefore, $H'$ is well-typed for~$K \cup K(\grave{\he})$.

Finally, in rule \RULE{R-Field-Assignment},~$\he" = \hl.\hf_i = \code{\hv'}$,
    $\grave{\he} = \code{\hv'}$,
    and~$H' = H[\hl \mapsto \code{C<NO,NI>(}[\hv'/\hv_i]\ol{\hv}\code{)}]$.
Note that~$K(\he") = K(\grave{\he}) = \{\}$, thus a if~$H'$ is well typed then it is well-typed for~$K \cup K(\grave{\he})$.
Because the typing rule \RULE{T-Field-Assignment} require that: \[
  K,\Gamma_H \vdash \hl.\hf : \hT
    \gap
  K,\Gamma_H \vdash \code{\hv'}:\code{T'}
    \gap
  K,\Gamma_H \vdash \code{T'} \st \hT
    \]
    then the heap~$H'$ is well-typed for~$K \cup K(\grave{\he})$.
\end{proof}



% \bibliographystyle{abbrv}
% \bibliography{bibstring-abbrev,igj-extra,alex,names,nicks,oopsla,ecoop}


\end{document}
